\begin{tabbing}
R{-}base{-}recognize($i$;${\it ds}$;$x$;$k$;$T$;${\it test}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(Rinit($i$;$\mathbb{B}$;$x$;inl ff ) $\oplus$ Rframe($i$;$\mathbb{B}$;$x$;[$k$ / []]))\+
\\[0ex]$\oplus$ \=Reffect($i$;fpf{-}join(IdDeq;$x$ : $\mathbb{B}$;${\it ds}$);$k$;$T$;$x$;inl ($\lambda$$s$,$v$. if ${\it test}$($s$,$v$)\+
\\[0ex]then tt
\\[0ex]else $s$($x$)
\\[0ex]fi ) )
\-\-
\end{tabbing}